00050	 VAR: x,y,z;INF_OP:⊗;
00075	INF_PRED: =; EQUALITY: =;
00100	G1: x⊗x = y⊗y;
00200	G2: x⊗(y⊗y) = x;
00300	G3: x⊗(y⊗z) = z⊗(y⊗x);
00400	G4: x⊗(x⊗y) = y;
00600	THEOREM:(x⊗z)⊗(y⊗z) = x⊗y;
00700	;